@i: x:T initially x = v(j) == if eqof(IdDeq)(j,i) x : T initially x = v else  fi 

latex

Definitions	x.A(x), if b t else f fi, f(a), eqof(d), IdDeq, x : t initially x = v,
FDL editor aliases	d-single-init